T:Type, Q:((T List)prop{i:l}).
Q([])
 (ys:(T List), y:T. Q(ys)  Q(append(ys; cons(y; []))))
 guard((zs:(T List). Q(zs))) 

latex

Definitions	t  T, x:A. B(x), x(s), P  Q, decidable(P), ||as||, ge(i; j), P  Q, False, A, A  B, , guard(T), prop{i:l}, append(as; bs), null(as), b, last(L), t  ...$L, P  Q, P  Q, P  Q, x:A. B(x)
Lemmas	last lemma, length append, length nil, length cons, last wf, ge wf, nat properties, append wf, nat wf, le wf, non neg length, length wf1, decidable assert, null wf